Nuprl Lemma : iseg_append
11,40
postcript
pdf
T
:Type,
l1
,
l2
,
l3
:(
T
List). iseg(
T
;
l1
;
l2
)
iseg(
T
;
l1
; append(
l2
;
l3
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
Lemmas
append
wf
origin
T:Type, l1,l2,l3:(T List). iseg(T; l1; l2) 
iseg(T; l1; append(l2; l3)) T:Type, l1,l2,l3:(T List). iseg(T; l1; l2) iseg(T; l1; append(l2; l3)) 
Tx:A. B(x)